#pragma once

#include <iostream>
#include <cctype>

#include "problem_factory.h"
#include "istrategy.h"
#include "problem_solver.h"
#include "file_data.h"

namespace sat
{

	class sat_solver_strategy : public solver::istrategy
	{
		static const int val_normal = 1;
		static const int val_not = 0;

	public:

		virtual int int_to_name(int k)
		{
			return k < -1 ? -k : k;
		}

		virtual solver::variable_value int_to_spin(int v)
		{
			if (v < 0) {
				return val_not;
			}
			return val_normal;
		}

		virtual void draw_production(Windows::UI::Xaml::Controls::Panel^ panel, solver::problem_solver* cur_problem, solver::production *cur_prod)
		{

			Windows::UI::Xaml::Controls::TextBlock^ tbTextBlock = ref new Windows::UI::Xaml::Controls::TextBlock();

			std::wstring implication_text = L"";

			if (cur_prod->product.ref == -1)
			{
				implication_text = L"conf <- ";
			}
			else
			{
				auto& v = cur_problem->variables[cur_prod->product.ref];
				if (cur_prod->product.val == val_not)
				{
					implication_text += L"!";
				}
				implication_text += std::to_wstring(v.name);
				implication_text += L" <- ";
			}

			for (int i = 0; i < cur_prod->match.size(); i++)
			{
				auto& l = cur_prod->match[i];
				auto& v = cur_problem->variables[l.ref];

				if (l.val == val_not)
				{
					implication_text += L"!";
					implication_text += std::to_wstring(v.name);
				}
				else {
					implication_text += std::to_wstring(v.name);
				}
			}

			Platform::String^ str = ref new Platform::String(implication_text.c_str());
			tbTextBlock->Text = str;

			panel->Children->Append(tbTextBlock);
		}

		virtual void draw_decision(Windows::UI::Xaml::Controls::Panel^ panel, solver::problem_solver* cur_problem, solver::decision& d, bool connector)
		{

			Windows::UI::Xaml::Controls::TextBlock^ tbTextBlock = ref new Windows::UI::Xaml::Controls::TextBlock();

			std::wstring text;

			text = L"(";

			for (int i = 0; i < d.literals.size(); i++)
			{
				auto& l = d.literals[i];
				auto& v = cur_problem->variables[l.ref];

				if (d.selected_literal == i) {
					text += L"*";
				}

				if (l.val == val_not)
				{
					text += L"!";
					text += std::to_wstring(v.name);
				}
				else {
					text += std::to_wstring(v.name);
				}

				if (i < d.literals.size() - 1) {
					text += L" V ";
				}
			}
			if (connector) {
				text += L") ^";
			}
			else {
				text += L")";
			}

			Platform::String^ str = ref new Platform::String(text.c_str());
			tbTextBlock->Text = str;

			panel->Children->Append(tbTextBlock);
		}

		virtual void draw_decision_string(Windows::UI::Xaml::Controls::Panel^ panel, solver::problem_solver* cur_problem, solver::decision_string& d)
		{
			Windows::UI::Xaml::Controls::TextBlock^ tbTextBlock = ref new Windows::UI::Xaml::Controls::TextBlock();
			std::wstring text;

			text = L"";
			bool written = false;
			int ds = d.size();
			for (int i = 0; i < ds; i++)
			{
				auto& vs = d[i];

				if (written) {
					text += L" ";
				}
				auto& v = cur_problem->variables[vs.ref];

				if (vs.val == val_not) {
					text += L"!";
					text += std::to_wstring(v.name);
				}
				else
				{
					text += std::to_wstring(v.name);
				}
				written = true;

			}

			Platform::String^ str = ref new Platform::String(text.c_str());
			tbTextBlock->Text = str;

			panel->Children->Append(tbTextBlock);
		}
	};

	class cnf_sat_solver
	{
		int current_line_number = 0;

		typedef const char *(cnf_sat_solver::*line_function)(const char *);
		line_function current_line_function;
		std::vector<int> current_clause;
		solver::problem_factory factory;
		int trace_variable = -1;

		const char *read_white(const char *cnf_file_contents)
		{
			while (*cnf_file_contents == ' ' || *cnf_file_contents == '\t')
				cnf_file_contents++;
			return cnf_file_contents;
		}

		const char *read_eol(const char *cnf_file_contents)
		{
			current_line_number++;
			while (*cnf_file_contents == '\r' || *cnf_file_contents == '\n')
				cnf_file_contents++;
			return cnf_file_contents;
		}

		bool is_eol(const char *cnf_file_contents)
		{
			return (*cnf_file_contents == '\r' || *cnf_file_contents == '\n' || *cnf_file_contents == 0);
		}

		const char *read_line(const char *cnf_file_contents)
		{
			cnf_file_contents = read_eol(cnf_file_contents);
			cnf_file_contents = read_white(cnf_file_contents);
			switch (*cnf_file_contents)
			{
			case 'P':
			case 'p':
				current_line_function = &cnf_sat_solver::read_problem_line;
				break;
			case 'C':
			case 'c':
				current_line_function = &cnf_sat_solver::read_comment_line;
				break;
			case 't': // our cnf supports a t variableid number that traces from that variable
				current_line_function = &cnf_sat_solver::read_trace_line;
				break;
			case '-':
			case '0':
			case '1':
			case '2':
			case '3':
			case '4':
			case '5':
			case '6':
			case '7':
			case '8':
			case '9':
				current_line_function = &cnf_sat_solver::read_clause_line;
				break;
			default:
				current_line_function = &cnf_sat_solver::read_other_line;
				std::cout << "line " << current_line_number << ": invalid line" << std::endl;
			}
			return cnf_file_contents;
		}

		const char *read_int(const char *cnf_file_contents, int *intr)
		{
			char buffer[256];
			int max_chars = sizeof(buffer) - 2;
			int count = 0;

			cnf_file_contents = read_white(cnf_file_contents);
			if (*cnf_file_contents == '-')
			{
				buffer[count++] = '-';
				cnf_file_contents++;
				cnf_file_contents = read_white(cnf_file_contents);
			}

			if (!std::isdigit(*cnf_file_contents))
			{
				std::cout << "line " << current_line_number << ": invalid integer" << std::endl;
				cnf_file_contents = read_other_line(cnf_file_contents);
				return cnf_file_contents;
			}

			while (std::isdigit(*cnf_file_contents) && count < max_chars)
			{
				buffer[count++] = *cnf_file_contents;
				cnf_file_contents++;
			}

			buffer[count++] = 0;
			*intr = strtol(buffer, nullptr, 10);

			return cnf_file_contents;
		}

		const char *read_problem_line(const char *cnf_file_contents)
		{
			while (!is_eol(cnf_file_contents))
				cnf_file_contents++;

			current_line_function = &cnf_sat_solver::read_line;

			return cnf_file_contents;
		}

		const char *read_comment_line(const char *cnf_file_contents)
		{
			while (!is_eol(cnf_file_contents))
				cnf_file_contents++;

			current_line_function = &cnf_sat_solver::read_line;

			return cnf_file_contents;
		}

		const char *read_clause_line(const char *cnf_file_contents)
		{

			while (!is_eol(cnf_file_contents))
			{
				int variable = 0;
				cnf_file_contents = read_int(cnf_file_contents, &variable);

				if (variable != 0)
				{
					current_clause.push_back(variable);
				}
				else
				{
					sat_solver_strategy strategy;
					factory.add_clause(0, current_clause.size(), &current_clause[0], &strategy);
					current_clause.clear();
				}
			}

			current_line_function = &cnf_sat_solver::read_line;

			return cnf_file_contents;
		}

		const char *read_trace_line(const char *cnf_file_contents)
		{
			cnf_file_contents++;
			if (!is_eol(cnf_file_contents))
			{
				int variable = 0;
				cnf_file_contents = read_int(cnf_file_contents, &variable);

				if (variable != 0)
				{
					trace_variable = variable;
				}
			}

			while (!is_eol(cnf_file_contents))
				cnf_file_contents++;

			current_line_function = &cnf_sat_solver::read_line;

			return cnf_file_contents;
		}

		const char *read_other_line(const char *cnf_file_contents)
		{
			while (!is_eol(cnf_file_contents))
				cnf_file_contents++;

			current_line_function = &cnf_sat_solver::read_line;

			return cnf_file_contents;
		}

	public:

		solver::problem_solver *create_problem(solver::file_data& data)
		{
			trace_variable = -1;

			const char *cnf_file_contents = data.get_data();

			solver::problem_solver *sat_prob = new solver::problem_solver();
			factory.clear();

			current_line_function = &cnf_sat_solver::read_line;

			while (*cnf_file_contents)
			{
				cnf_file_contents = (this->*current_line_function)(cnf_file_contents);
			}

			factory.create_problem(*sat_prob, trace_variable, data.get_file_name().c_str());

			sat_prob->trace_enabled = trace_variable > -1;

			return sat_prob;
		}

		bool solve(solver::file_data& data, bool dump)
		{
			auto sat_prob = create_problem(data);

			sat_solver_strategy strategy;

			sat_prob->solve(strategy);

			delete sat_prob;

			return true;
		}
	};
}

